Problem: a(a(x1)) -> b(b(x1)) a(b(x1)) -> c(c(x1)) b(c(x1)) -> a(a(x1)) Proof: Bounds Processor: bound: 2 enrichment: match automaton: final states: {3,2} transitions: a1(7) -> 8* a1(8) -> 9* b2(10) -> 11* b2(11) -> 12* a0(1) -> 2* b0(1) -> 3* c0(1) -> 1* 1 -> 7* 7 -> 10* 9 -> 11,3 12 -> 9,3 problem: Qed